nLab Steve Zdancewic

• personal page

Selected writings

On linear algebra (finite-dimensional vector spaces over finite fields) as categorical semantics for linear logic/linear type theory:

• Benoît Valiron, Steve Zdancewic, Finite Vector Spaces as Model of Simply-Typed Lambda-Calculi, in: Proc. of ICTAC’14, Lecture Notes in Computer Science 8687, Springer (2014) 442-459 [arXiv:1406.1310, doi:10.1007/978-3-319-10882-7_26, slides:pdf, pdf]

Introducing QWIRE, a quantum programming language based on linear type theory connected with intuitionistic type theory via the exponential modality:

• Jennifer Paykin, Robert Rand, Steve Zdancewic, QWIRE: a core language for quantum circuits, POPL 2017: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming LanguagesJanuary 2017 Pages 846–858 (doi:10.1145/3009837.3009894)

Application to verified programming after implementation in Coq:

• Robert Rand, Jennifer Paykin, Steve Zdancewic, QWIRE Practice: Formal Verification of Quantum Circuits in Coq, EPTCS 266, 2018, pp. 119-132 (arXiv:1803.00699)

• Robert Rand, Jennifer Paykin, Dong-Ho Lee, Steve Zdancewic, ReQWIRE: Reasoning about Reversible Quantum Circuits, EPTCS 287 (2019) 299-312 [arXiv:1901.10118, doi:10.4204/EPTCS.287.17]

Using ambient homotopy type theory:

• Jennifer Paykin, Steve Zdancewic, A HoTT Quantum Equational Theory, talk at QPL2019 [arXiv:1904.04371, pdf, pdf]

category: people